COMMENT ⊗   VALID 00011 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	cuts
C00009 00003	addition of cuts
C00011 00004	(proof commutcutadd)
C00012 00005	(proof assoc_cutadd)
C00014 00006	(proof classes)
C00016 00007	proof of facts about cuts: cut extensionality, totalcut1, antisymlesscut
C00019 00008	proof of facts about pluscut: nonempty loweclass, -upperclass
C00021 00009	proof pluscut_totalcut
C00028 00010	proof pluscut_dense
C00030 00011	to finish
C00039 ENDMK
C⊗;
;cuts
(wipe-out)
(get-proofs rat1 prf ekl sys)

(proof cuts)
(decl (ratset) (type: |@r→truthval|)(syntype: variable))

;definition of cut
(decl (cut)(type: |@ratset→truthval|)(syntype: constant))
(define cut |∀ratset.cut(ratset)≡
                     (∃r.ratset r)∧(∃r.¬ratset r)∧
                     (∀r s.ratset r∧¬ratset s⊃r<s)∧
                     (∀r.ratset r⊃(∃s.ratset s∧s>r))|)
(label cutdefinition)

(decl (|α!| |β!| |α!0| |α!1| |α!2|) (type: |@ratset|) (sort: cut))

(axiom |∀α!.∃r.α!(r)|)
(label cutdef)(label nonempty_lowercl)

(axiom |∀α!.∃r.¬(α!)(r)|)
(label cutdef)(label nonempty_uppercl)

(axiom |∀α! s r.α!(s)∧¬α!(r)⊃s<r|)
(label cutdef)(label totalcut)

(axiom |∀α! r.α!(r)⊃∃s.r<s∧α!(s)|)
(label cutdef)(label densecut)

(axiom |∀arb α!.arbεα!⊃ratio(arb)|)
(label cutmember_sort)

;equality of cuts is equality of sets
;Landau_th116,117,118 are property of equality.

;(ue ((setvar.|α!|)(setvar1.|β!|)) set_extensionality)
;(∀ARB.ARBεα!≡ARBεβ!)⊃α!=β!
(axiom |(∀arb.arbεα!≡arbεβ!)⊃α!=β!|)
(label cut_ext)

(axiom |∀α! β!.(∀r.rεα!≡rεβ!)⊃α!=β!|)
(label cut_extensionality)

;Landau_th119
;(derive |∀α!.∀r s.¬α!(r)∧r<s⊃¬α!(s)| (totalcut antisymlessrat))
(axiom |∀α!.∀r s.¬α!(r)∧s>r⊃¬α!(s)|)
(label upperclass)

;Landau_th120
;(derive |∀α!.∀r s.α!(r)∧s<r⊃α!(s)| * (use inconsistent mode: always)
;        (use grat_lrat mode: exact direction: reverse))
(axiom |∀α!.∀r s.α!(r)∧s<r⊃α!(s)|)
(label lowerclass)

;(derive |(∀r r1.rεα!∧r1≤r⊃r1εα!)≡(∀r r1.rεα!∧¬r1εα!⊃r1>r)|
;        totalordrat (open leqrat))

;(rw * (use grat_lrat mode: exact))
;(∀r r1.rεα!∧r1 ≤ r⊃r1εα!)≡(∀r r1.rεα!∧¬r1εα!⊃r < r1)
;(label totalcut1)

;greater than 
(decl gc (type: |@ratset⊗@ratset→truthval|)
      (syntype: constant)(bindingpower: 935))
(defax gc |∀α! β!.gc(α!,β!)≡∃r.α!(r)∧¬β!(r)|)

;less than 
(decl lc (type: |@ratset⊗@ratset→truthval|)
      (syntype: constant)(bindingpower: 935))
(defax lc |∀α! β!.lc(α!,β!)≡∃r.¬α!(r)∧β!(r)|)

;Landau_th121
;(trw |lc(α!,β!)⊃gc(β!,α!)| (open lc gc))
(axiom |∀α! β!.lc(α!,β!)⊃gc(β!,α!)|)
(label lessgreatcut)

;Landau_th122
;(trw |gc(α!,β!)⊃lc(β!,α!)| (open lc gc))
(axiom |∀α! β!.gc(α!,β!)⊃lc(β!,α!)|)
(label greatlesscut)

;(derive |∀α! β!.gc(α!,β!)≡lc(β!,α!)| (greatlesscut lessgreatcut))
(axiom |∀α! β!.gc(α!,β!)≡lc(β!,α!)|)
(label gc_lc)

;Landau_th123
;(trw |∀α! β!.¬(α!=β!∧lc(α!,β!))| (open lc))
(axiom |∀α! β!.¬(α!=β!∧lc(α!,β!))|)
(label noteqless)

;(trw |∀α! β!.¬(α!=β!∧gc(α!,β!))| (open gc))
(axiom |∀α! β!.¬(α!=β!∧gc(α!,β!))|)
(label noteqgreat)

(axiom |∀α! β!.¬(lc(α!,β!)∧lc(β!,α!))|)
(label antisymlesscut)
;see proof below

;totalordcut
;proof in two lines!!!

;(derive |¬α!=β!⊃lc(β!,α!)∨lc(α!,β!)| (cut_extensionality) (open lc))
;(label totalordcut1)

;(derive |lc(α!,β!)∨α!=β!∨gc(α!,β!)| (* lessgreatcut))
(axiom |∀α! β!.lc(α!,β!)∨α!=β!∨gc(α!,β!)|)
(label totalordcut)

;Landau_def32
(decl gec (type: |@ratset⊗@ratset→truthval|)
      (syntype: constant)(bindingpower: 935))
(define gec |∀α! β!.gec(α!,β!)≡α!=β!∨gc(α!,β!)|)

;Landau_def33
(decl lec (type: |@ratset⊗@ratset→truthval|)
      (syntype: constant)(bindingpower: 935))
(define lec |∀α! β!.lec(α!,β!)≡α!=β!∨lc(α!,β!)|)

;Landau_th124 125
;(trw |∀α! β!.gec(α!,β!)≡lec(β!,α!)| 
;     (use gc_lc mode: exact)(open gec lec))
(axiom |∀α! β!.gec(α!,β!)≡lec(β!,α!)|)
(label gec_lec)

;Landau_th126
;(trw |∀α! α!0 α!1.lc(α!,α!0)∧lc(α!0,α!1)⊃lc(α!,α!1)| 
;     (open lc) (transordrat))
(axiom |∀α! α!0 α!1.lc(α!,α!0)∧lc(α!0,α!1)⊃lc(α!,α!1)|)
;∀α! α!0 α!1.LC(α!,α!0)∧LC(α!0,α!1)⊃LC(α!,α!1)
(label transordcut)

;Landau_th127
(axiom |∀α! α!0 α!1.lec(α!,α!0)∧lc(α!0,α!1)⊃lc(α!,α!1)|)
(label Landau_a_th127)
;exercise

(axiom |∀α! α!0 α!1.lc(α!,α!0)∧lec(α!0,α!1)⊃lc(α!,α!1)|)
(label Landau_b_th127)
;exercise

;Landau_th128
(axiom |∀α! α!0 α!1.lec(α!,α!0)∧lec(α!0,α!1)⊃lec(α!,α!1)|)
(label translec)
(show *)
;addition of cuts
(proof pluscut)

;Landau_def34
(decl (pc) (type: |@ratset⊗@ratset→@ratset|) 
      (syntype: constant) (bindingpower: 975))
(define pc |∀α! β!.pc(α!,β!)=(λr.(∃r1 r2.α!(r1)∧β!(r2)∧r=r1+r2))|)
(label pluscutdef)

;(trw |∀α! β! r1 r2.α!(r1)∧β!(r2)⊃(pc(α!,β!))(r1 + r2)| (open pc))
(axiom |∀α! β! r1 r2.α!(r1)∧β!(r2)⊃(pc(α!,β!))(r1 + r2)|)
(label pluscutdef1)

;Landau_th129
;verification that pc is well defined

(axiom |∀α! β!.∃r2.(pc(α!,β!))(r2)|)
(label pluscutdef)(label pluscut_nel)
;see proof below

(axiom |∀α! β!.∃r.¬(pc(α!,β!))(r)|)
(label pluscutdef)(label pluscut_neu)
;see proof below

(axiom |∀α! β! s r.(pc(α!,β!))(r)∧s<r⊃(pc(α!,β!))(s)|)
(label pluscutdef)(label pluscut_tc)
;see proof below

(axiom |∀α! β! r.(pc(α!,β!))(r)⊃∃s.r<s∧(pc(α!,β!))(s)|)
(label pluscutdef)(label pluscut_dc)
;see proof below

(axiom |∀α! β!.cut(pc(α!,β!))|)
(label pluscutsort) (label simpinfo)
;exercise

;Landau_th130
(axiom |∀α! β!.pc(α!,β!)=pc(β!,α!)|)
(label commutcutadd)
;see proof below

(axiom |∀α! α!0 α!1.pc(pc(α!,α!0),α!1)=pc(α!,pc(α!0,α!1))|)
(label assoc_cutadd)
(proof commutcutadd)
(assume |(pc(α!,β!))(r)|)
(label commcut1)

(rw * (open pc))
;∃R1 R2.α!(R1)∧β!(R2)∧R=R1+R2
;deps: (COMMCUT1)

(define rx1 |∃r2.α!(rx1)∧β!(r2)∧r=rx1+r2| *)

(define rx2 |α!(rx1)∧β!(rx2)∧r=rx1+rx2| *)

(derive |β!(rx2)∧α!(rx1)∧r=rx2+rx1| * (use commaddrat mode: exact))

(trw |(pc(β!,α!))(r)| (open pc) *)
;(PC(β!,α!))(R)
;deps: (COMMCUT1)

(ci commcut1)
;(PC(α!,β!))(R)⊃(PC(β!,α!))(R)

(ue ((α!.β!)(β!.α!)) *)
;(PC(β!,α!))(R)⊃(PC(α!,β!))(R)

(derive |pc(α!,β!)=pc(β!,α!)| (* -2 cut_extensionality))

(proof assoc_cutadd)

(assume |(pc(pc(α!,α!0),α!1))(r)|)
(label ascut1)

(rw * (use pluscutdef mode: exact))
;∃R1 R2.(∃R3 R4.α!(R3)∧α!0(R4)∧R1=R3+R4)∧α!1(R2)∧R=R1+R2
;deps: (ASCUT1)

;we shouldn't need this

(define rv1 |∃r2.(∃r3 r4.α!(r3)∧α!0(r4)∧rv1=r3+r4)∧α!1(r2)∧r=rv1+r2| *)
(define rv2 |(∃r3 r4.α!(r3)∧α!0(r4)∧rv1=r3+r4)∧α!1(rv2)∧r=rv1+rv2| *)
(label ascut2)

(define rv3 |∃r4.α!(rv3)∧α!0(r4)∧rv1=rv3+r4| *)
(define rv4 |α!(rv3)∧α!0(rv4)∧rv1=rv3+rv4| *)
(label ascut3)

(rw ascut2 (use * mode: always))
;α!1(RV2)∧R=RV3+RV4+RV2
;deps: (ASCUT1)

(derive |α!(rv3)∧α!0(rv4)∧α!1(rv2)∧r=rv3+rv4+rv2| (ascut3 *))
(label ascut4)

(derive |(∃r1 r2.α!(r1)∧(∃r5 r6.α!0(r5)∧α!1(r6)∧r2=r5+r6)∧r=r1+r2)| *)

(trw |(pc(α!,pc(α!0,α!1)))(r)| (use pluscutdef mode: always) *)
;(PC(α!,PC(α!0,α!1)))(R)
;deps: (ASCUT1)

(ci ASCUT1)
;(PC(PC(α!,α!0),α!1))(R)⊃(PC(α!,PC(α!0,α!1)))(R)
(label assoc_cutadd)
(proof classes)
(unlabel SIMPINFO MINUSSORT)

;(axiom |∀α! s.s≠0⊃(∃r r1.¬α!(r)∧α!(r1)∧r1+s=r)|)

(define rxv |α!(rxv)| nonempty_lowercl)
(label cl1)

(define ryv |¬α!(ryv)| nonempty_uppercl)
(label cl2)

(derive |rxv<ryv| (cl1 cl2 totalcut))
(label cl3)

(assume |s≠0|)
(label cl4)

(ue ((r.ryv)(s.rxv)) minussort cl3 
    (use leqratdefinition mode: exact))
;RATIO(RYV-RXV)

(define nxv |nxv≠0∧nxv*s>(ryv-rxv)| (* cl4 Landau_th115))
(label cl5)

(deletel *)
(show landau_th115)
(derive |¬α!(nxv*s)| (* cl2 upperclass))


;(axiom |∀α! s.s≠0⊃(∃r r1.¬α!(r)∧α!(r1)∧r1+s=r)|)

(trw |rxv+ryv=ryv| *)
;RXV+RYV=RYV
;deps: (CL4)

;labels: LANDAU_TH115 
;∀R R1.¬R=0⊃(∃N.¬N=0∧N*R>R1)

(show Landau_th115)
(derive |(∃r r1.¬α!(r)∧α!(r1)∧r1+s=r)|(cl1 cl2 *))
;proof of facts about cuts: cut extensionality, totalcut1, antisymlesscut
(proof cut_extensionality)

;cutmember_sort
;∀r α!.rεα!⊃ratio(r)

(assume |∀r.rεα!≡rεβ!|)
(derive |∀r.rεα!⊃rεβ!| *)

(assume |arbεα!|)
(derive |ratio(arb)| (* cutmember_sort))
(trw |arbεβ!| (-3 -2) (use * mode: always))
;ARBεr1
(ci (-5 -3))
;(∀r.rεα!≡rεβ!)∧ARBεα!⊃ARBεβ!

(ue ((r.r1)(r1.r)) *)
;(∀r.rεα!≡rεβ!)∧ARBεα!⊃ARBεβ!
(derive |(∀r.rεα!≡rεβ!)⊃(arbεα!⊃arbεβ!)| -2)
(derive |(∀r.rεα!≡rεβ!)⊃(arbεβ!⊃arbεα!)| -2)
(derive |(∀r.rεα!≡rεβ!)⊃(arbεα!≡arbεβ!)| (* -2))
;(derive |(∀r.rεα!≡rεβ!)≡(∀arb.arbεα!≡arbεβ!)| *)

;antisymlesscut

(assume |lc(α!,β!)∧lc(β!,α!)|)
(rw * (open lc))
;(∃r.¬α!(r)∧β!(r))∧(∃r.¬β!(r)∧α!(r))

(define rv |¬α!(rv)∧β!(rv)| *)

(define rw |¬β!(rw)∧α!(rw)| -2)

;labels: CUTDEF TOTALCUT 
;(axiom |∀α! s r.α!(s)∧¬α!(r)⊃s < r|)

(ue ((α!.α!)(s.rw)(r.rv)) totalcut * -2)
;rW < rV

(ue ((α!.β!)(s.rv)(r.rw)) totalcut -2 -3)
;rV < rW

(derive |false| (* -2 antisymlessrat))

(ci -7)
;¬(LC(α!,β!)∧LC(β!,α!))
;proof of facts about pluscut: nonempty loweclass, -upperclass

(proof pluscutfacts)
;nonempty lowerclass

(define rw1 |α!(rw1)| nonempty_lowercl)
(label nc1)
(define rw2 |β!(rw2)| nonempty_lowercl)
(label nc2)
(trw |(pc(α!,β!))(rw1 + rw2)| (open pc) nc1 nc2)
;(PC(α!,β!))(RW1+RW2)
(derive |∃r2.(pc(α!,β!))(r2)| *)
(derive |∀α! β!.∃r2.(pc(α!,β!))(r2)| (*))

;nonempty upperclass

(define rw3 |¬α!(rw3)| nonempty_uppercl)
(label nuc1)

(define rw4 |¬β!(rw4)| nonempty_uppercl)
(label nuc2)

(assume |α!(r)∧β!(r1)|)
(label nuc3)

;labels: GRAT_LRAT 
;∀r r1.r > r1≡r1 < r

(derive |rw3>r∧rw4>r1| (nuc1 nuc2 nuc3 totalcut)
        (use grat_lrat mode: exact))
(label nuc4)

;labels: GREAT_GREAT_ADDRATPRESERVING 
;∀r s r1 r2.r1 > r∧r2 > s⊃r1 + r2 > r + s

(ue ((r.r)(s.r1)(r1.rw3)(r2.rw4)) 
    great_great_addratpreserving *)
;RW3+RW4>R+R1
;deps: (NUC3)


(trw |(rw3+rw4)≠(r+r1)| (* strictrat2))
;¬RW3+RW4=R+R1
;deps: (NUC3)

(ci nuc3)
;α!(R)∧β!(R1)⊃¬RW3+RW4=R+R1

(derive |¬∃r s.α!(r)∧β!(s)∧r + s=rw3 + rw4| *)

(derive |¬(pc(α!,β!))(rw3+rw4)| * (open pc))

(derive |∃r.¬(pc(α!,β!))(r)| *)
;end of the proof nonempty_uppercl
;proof pluscut_totalcut

;want:   
;∀α! β! s r.(pc(α!+β!))(r)∧s<r⊃(pc(α!+β!))(s)
;(label pluscutdef)(label pluscut_tc)

(proof pluscut_totalcut)

1.  (assume |(pc(α!,β!))(r)|)
    (label pc_tc1)

2.  (rw * (open pc))
    ;∃R1 R2.α!(R1)∧β!(R2)∧R=R1+R2
    ;deps: (PC_TC1)

3.  (define ry1 |∃r2.α!(ry1)∧β!(r2)∧r=ry1 + r2| *)
    ;RY1 is unknown.
    ;the symbol RY1 is given the same declaration as R
    ;deps: (PC_TC1)

4.  (define ry2 |α!(ry1)∧β!(ry2)∧r=ry1 + ry2| *)
    ;RY2 is unknown.
    ;the symbol RY2 is given the same declaration as R
    ;deps: (PC_TC1)
    (label pc_tc2)

5.  (assume |s<r|)
    (label pc_tc3)

6.  (assume |ry1 = 0|)
    (label pc_tc4)

7.  (trw |r=ry2| (use pc_tc2 pc_tc4 mode: always) add_rzero)
    ;R=RY2
    ;deps: (PC_TC1 PC_TC4)

8.  (trw |β!(r)| pc_tc2 (use * mode: exact))
    ;β!(R)
    ;deps: (PC_TC1 PC_TC4)

9.  (trw |β!(s)| (lowerclass pc_tc3 *))
    ;β!(S)
    ;deps: (PC_TC1 PC_TC3 PC_TC4)

10. (trw |(pc(α!,β!))(ry1 + s)| (pluscutdef1 pc_tc2 *))
    ;(PC(α!,β!))(RY1+S)
    ;deps: (PC_TC1 PC_TC3 PC_TC4)

11. (rw * (use pc_tc4 mode: exact))
    ;(PC(α!,β!))(S)
    ;deps: (PC_TC1 PC_TC3 PC_TC4)
    (label pc_tc5)

    ;second case

13. (assume |ry2 = 0|)
    (label pc_tc6)

14. (trw |r=ry1| (use pc_tc2 pc_tc6 mode: always) add_rzero)
    ;R=RY1
    ;deps: (PC_TC1 PC_TC6)

15. (trw |α!(r)| pc_tc2 (use * mode: exact))
    ;α!(R)
    ;deps: (PC_TC1 PC_TC6)

16. (trw |α!(s)| (lowerclass pc_tc3 *))
    ;α!(S)
    ;deps: (PC_TC1 PC_TC3 PC_TC6)

17. (trw |(pc(α!,β!))(s + ry2)| (pluscutdef1 pc_tc2 *))
    ;(PC(α!,β!))(S+RY2)
    ;deps: (PC_TC1 PC_TC3 PC_TC6)

18. (rw * (use pc_tc6 mode: exact))
    ;(PC(α!,β!))(S)
    ;deps: (PC_TC1 PC_TC3 PC_TC6)
    (label pc_tc7)

    ;third case
19. (assume |ry1 ≠ 0 ∧ ry2 ≠ 0|)
    (label pc_tc10)

    ;labels: RZEROLEAST 
    ;∀R.¬R<0

20. (derive |r≠0| (rzeroleast pc_tc3))
    ;deps: (PC_TC3)
    (label pc_tc11)

    ;labels: DIVISIONRAT 
    ;∀R R1.¬R1=0⊃R1*DIV(R,R1)=R

21. (ue ((r.s)(r1.r)) divisionrat * divsort)
    ;R*DIV(S,R)=S
    ;deps: (PC_TC3)

22. (trw |r*(div(s,r))<r| (pc_tc3 *) divsort)
    ;R*DIV(S,R)<R
    ;deps: (PC_TC3)

    ;labels: LESS_LMULTRATPRESERVING 
    ;∀R R1 R2.¬R2=0⊃R<R1≡R2*R<R2*R1

23. (ue ((r.|div(s,r)|)(r1.|1|)(r2.r)) less_lmultratpreserving 
	pc_tc11 *)
    ;DIV(S,R)<1
    ;deps: (PC_TC3)
    (label pc_tc12)

24. (ue ((r.|div(s,r)|)(r1.|1|)(r2.ry1)) less_lmultratpreserving 
        pc_tc10 pc_tc11 *)
    ;RY1*DIV(S,R)<RY1
    ;deps: (PC_TC3 PC_TC10)
    (label pc_tc13)

    ;labels: LOWERCLASS 
    13. (AXIOM |∀α!.(∀R S.α!(R)∧S<R⊃α!(S))|)

26. (ue ((α!.α!)(r.|ry1|)(s.|ry1*div(s,r)|)) lowerclass
	pc_tc2 * pc_tc11)
    ;α!(RY1*DIV(S,R))
    ;deps: (PC_TC1 PC_TC3 PC_TC10)
    (label pc_tc14)

26. (ue ((r.|div(s,r)|)(r1.|1|)(r2.ry2)) less_lmultratpreserving 
	pc_tc10 pc_tc11 pc_tc12)
    ;RY2*DIV(S,R)<RY2
    ;deps: (PC_TC3 PC_TC10)
    (label pc_tc15)

27. (ue ((α!.β!)(r.|ry2|)(s.|ry2*div(s,r)|)) lowerclass
	pc_tc2 * pc_tc11)
    ;β!(RY2*DIV(S,R))
    ;deps: (PC_TC1 PC_TC3 PC_TC10)
    (label pc_tc16)

28. (trw |(pc(α!,β!))((ry1*div(s,r))+(ry2*div(s,r)))| pluscutdef1 
	 pc_tc14 pc_tc16 pc_tc11)
    ;(PC(α!,β!))(RY1*DIV(S,R)+RY2*DIV(S,R))
    ;deps: (PC_TC1 PC_TC3 PC_TC10)
    (label pc_tc17)

    ;labels: RDISTRAT 
    ;∀R0 R1 R2.(R1+R2)*R0=R1*R0+R2*R0

29. (ue ((r0.|div(s,r)|)(r1.|ry1|)(r2.|ry2|)) rdistrat pc_tc11)
    ;(RY1+RY2)*DIV(S,R)=RY1*DIV(S,R)+RY2*DIV(S,R)
    ;deps: (PC_TC3)

30. (rw pc_tc17 (use * mode: always direction: reverse))
    ;(PC(α!,β!))((RY1+RY2)*DIV(S,R))
    ;deps: (PC_TC1 PC_TC3 PC_TC10)

31. (rw * (use pc_tc2 mode: always direction: reverse))
    ;(PC(α!,β!))(R*DIV(S,R))
    ;deps: (PC_TC1 PC_TC3 PC_TC10)

32. (rw * (use divisionrat mode: always) pc_tc11)
    ;(PC(α!,β!))(S)
    ;deps: (PC_TC1 PC_TC3 PC_TC10)
    (label pc_tc18)

33. (trw |ry1 = 0 ∨ ry2 = 0 ∨ (ry1 ≠ 0 ∧ ry2 ≠ 0)|)
    ;RY1=0∨RY2=0∨¬RY1=0∧¬RY2=0

34. (cases * pc_tc5 pc_tc7 pc_tc18)
    ;(PC(α!,β!))(S)
    ;deps: (PC_TC1 PC_TC3)

35. (ci (pc_tc1 pc_tc3))
    ;(PC(α!,β!))(R)∧S<R⊃(PC(α!,β!))(S)

;proof pluscut_dense
(proof pluscut_dense)

1.  (assume |(pc(α!,β!))(r)|)
    (label pcd1)

2.  (rw * (open pc))
    ;∃R1 R2.α!(R1)∧β!(R2)∧R=R1+R2
    ;deps: (PCD1)

3.  (define ry1 |∃r2.α!(ry1)∧β!(r2)∧r=ry1 + r2| *)
    ;RY1 is unknown.
    ;the symbol RY1 is given the same declaration as R
    ;deps: (PCD1)

4.  (define ry2 |α!(ry1)∧β!(ry2)∧r=ry1 + ry2| *)
    ;RY2 is unknown.
    ;the symbol RY2 is given the same declaration as R
    ;deps: (PCD1)
    (label pcd2)

5.  (ue ((α!.α!)(r.ry1)) densecut *)
    ;∃S.RY1<S∧α!(S)
    ;deps: (PCD1)

6.  (define sy |ry1<sy∧α!(sy)| (densecut *))
    (label pcd3)

    ;labels: LESS_RADDRATPRESERVING 
    ;∀R S R1.R<S≡R+R1<S+R1

7.  (ue ((r.ry1)(s.sy)(r1.ry2)) less_raddratpreserving *)
    ;RY1+RY2<SY+RY2
    ;deps: (PCD1)
    (label pcd4)

8.  (trw |(pc(α!,β!))(sy+ry2)| (pluscutdef1 pcd3 pcd2))
    ;(PC(α!,β!))(SY+RY2)
    ;deps: (PCD1)
    (label pcd5)

9.  (derive |∃s.r<s∧(pc(α!,β!))(s)| (pcd4 pcd5) 
            (use pcd2 mode: always))
    ;deps: (PCD1)

10. (ci pcd1)
    ;(PC(α!,β!))(R)⊃(∃S.R<S∧(PC(α!,β!))(S))

;to finish

;;;;(trw |∀α! β!.cut(a!plβ!)|)
;
;;;;(trw |∀α! β!.∀r s.¬α!(r)∧¬β!(s)⊃¬α!plβ!(r+s)|)
;
;;;;(trw |∀α! β!.α!plβ!=β!plα!|)
;
;;;;(trw |∀α1! α2! α3!.(α1!plα2!)plα3!=α1!pl(α2!plα3!)|)
;
;;;;(trw |∀α!.∀s.∃r1 r2.α!(r1)∧¬α!(r2)∧r1+s=r2|)